From Coq Require Import Arith Lia String.
Open Scope string_scope.
Import Nat.
Require Import List.
Import ListNotations.


Inductive lt: nat -> nat -> Prop :=
| lt_next: forall n, lt n (S n)
| lt_skip: forall n m (LT: lt n m), lt n (S m).

Lemma lt36:
  lt 3 6.
Proof.
  apply lt_skip. apply lt_skip. apply lt_next.
Qed.

(* TC : Transitive Closure *)
Inductive tc {A} (R : A -> A -> Prop) : A -> A -> Prop :=
| TcBase : forall x y, R x y -> tc R x y
| TcTrans : forall x y z, tc R x y -> tc R y z -> tc R x z.

Definition oneApart (n m : nat) : Prop :=
  n + 1 = m.

Definition lt' : nat -> nat -> Prop := tc oneApart.

Inductive person : Type :=
| Hera
| Ares
| Hephaestus
| Eros.

Inductive parent_of: person -> person -> Prop :=
| he_ar: parent_of Hera Ares
| he_he: parent_of Hera Hephaestus
| ar_er: parent_of Ares Eros.

Definition ancestor_of : person -> person -> Prop :=
  tc parent_of.

Inductive useless: nat -> Prop := .

Inductive total_relation : nat -> nat -> Prop :=
  | tot n m : total_relation n m.

Inductive ev : nat -> Prop :=
  | ev_0: ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).


Theorem lt'_lt : forall n m, lt' n m -> n < m.
Proof.
Admitted.


Lemma lt'_O_S : forall m, lt' 0 (S m).
Proof.
Admitted.


Lemma lt_lt'' : forall n k, lt' n (S k + n).
Proof.
Admitted.


Theorem lt_lt' : forall n m, n < m -> lt' n m.
Admitted.


(** ** Transitive closure is idempotent. *)
Theorem tc_tc2 : forall A (R : A -> A -> Prop) x y, tc R x y -> tc (tc R) x y.
Proof.
Admitted.


Theorem tc2_tc : forall A (R : A -> A -> Prop) x y, tc (tc R) x y -> tc R x y.
Proof.
Admitted.

(*|

Let's define inductively list permutations.
This example is directly taken from the Coq standard library.

|*)

Inductive Permutation {A} : list A -> list A -> Prop :=
| perm_nil :
    Permutation [] []
| perm_skip : forall x l l',
    Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap : forall x y l,
    Permutation (y::x::l) (x::y::l)
| perm_trans : forall l l' l'',
    Permutation l l' -> Permutation l' l'' -> Permutation l l''.

Lemma permut_test:
  Permutation [3;4;5] [5;4;3].
Proof.
Admitted.

Lemma Permutation_to_front : forall A (a : A) (ls : list A),
    Permutation (a :: ls) (ls ++ [a]).
Proof.
Admitted.

Theorem Permutation_rev : forall A (ls : list A),
    Permutation ls (rev ls).
Proof.
Admitted.

Theorem Permutation_length : forall A (ls1 ls2 : list A),
    Permutation ls1 ls2 -> length ls1 = length ls2.
Proof.
Admitted.

Lemma Permutation_refl : forall A (ls : list A),
    Permutation ls ls.
Proof.
Admitted.

Lemma Permutation_app1 : forall A (ls1 ls2 ls : list A),
    Permutation ls1 ls2
    -> Permutation (ls1 ++ ls) (ls2 ++ ls).
Proof.
Admitted.


Lemma Permutation_app2 : forall A (ls ls1 ls2 : list A),
    Permutation ls1 ls2
    -> Permutation (ls ++ ls1) (ls ++ ls2).
Proof.
Admitted.


Theorem Permutation_app : forall A (ls1 ls1' ls2 ls2' : list A),
    Permutation ls1 ls1'
    -> Permutation ls2 ls2'
    -> Permutation (ls1 ++ ls2) (ls1' ++ ls2').
Proof.
Admitted.


(* Bonus exercise: we could have defined Permutation with a function,
   for instance checking that both list are equal after being sorted.
   Do you think some of these lemmas would have been equally easy to prove? *)

(*|

Even more examples

|*)

Theorem ev_minus2 : forall n,
      ev n -> ev (pred (pred n)).
Proof.
Admitted.


Theorem evSS_ev_remember : forall n,
    ev (S (S n)) -> ev n.
Proof.
Admitted.

Theorem inversion_ex1 : forall (n m o : nat),
  [n; m] = [o; o] -> [n] = [m].
Proof.
Admitted.

Theorem inversion_ex2 : forall (n : nat),
  S n = O -> 2 + 2 = 5.
Proof.
Admitted.

Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
Proof.
Admitted.


(* Next question: define an inductive relation between two lists stating that one is a subsequence of the other. *)
Inductive subseq : list nat -> list nat -> Prop :=
(* TODO *)
.

Theorem subseq_refl : forall (l : list nat), subseq l l.
Proof.
Admitted.

Theorem subseq_app : forall (l1 l2 l3 : list nat),
  subseq l1 l2 ->
  subseq l1 (l2 ++ l3).
Proof.
Admitted.

Theorem subseq_trans : forall (l1 l2 l3 : list nat),
  subseq l1 l2 ->
  subseq l2 l3 ->
  subseq l1 l3.
Proof.
  (* Hint: be careful about what you are doing induction on and which
     other things need to be generalized... *)
Admitted.